A:Type, I:MaInterface(A), i:{i:Id| (i  fpf-domain(I))} .
(I(i).2)  k:{k:Knd| hasloc(k;i)}  fp V:Type  Top 

latex

Definitions	Id, MaInterface(T), Top, a:A fp B(a), t  T, x:AB(x), x:A. B(x), fpf-domain(f), (x  l), {x:A| B(x)} , f(x), t.2, Knd, b, Type, x:A  B(x), P  Q, IdDeq, left + right, State(ds), hasloc(k;i), s = t, x. t(x), type List, Void, x:A.B(x), x.A(x), <a, b>
Lemmas	ma-interface-type-trivial, fpf-trivial-subtype-top, subtype rel function, subtype rel product, Id wf, fpf wf, Knd wf, assert wf, hasloc wf, decl-state wf, top wf, ma-interface-apply-type, l member wf, fpf-domain wf